Dave:

	What  follows  is  the best I can do in the time available on
writing up a plan for basic research in formal reasoning.  It is hard
to  be non-technical and concise at the same time, and also I haven't
thought enough about the 78-80 time frame. Because much of  the  work
is theoretical, its first impact will most likely be in adding to the
intellectual base of more applied work in AI.  On the one hand, it is
easy  to  be  skeptical about a particular claim of this kind, and on
the other hand, applied work really is dependent in every science  on
the basic and theoretical work.

	Your  request  for  a Scientific American level report on FOL
will be easier to write, because it can be somewhat  longer  and  the
topic  is  more limited.  I hope to discuss your requirements in this
regard on Thursday.  I have referred the  natural  language  part  to
Terry Winograd.  It may be that he has already written something that
may be suitable, but I guess I doubt it.

********************

FIVE YEAR PLAN FOR FORMAL REASONING (first draft)


	Basic   artificial  intelligence  work  in  formal  reasoning
includes three lines of investigation.

	1.  What are the common sense facts about the world  and  how
can  they be represented suitably in the memory of a computer?    For
example, if AI is to be applied to a program that advises a commander
on how to use his missiles, the program needs to be able to represent
certain facts about its own knowledge and that  of  its  friends  and
foes.    Thus it might have to know the following: "We will know what
airplanes are in area A (by radar), but not in area  B.    The  enemy
will  not  know  the location of our ships unless he gets an observer
close enough".   It must be able to  derive  such  facts  from  other
facts,  e.g. from observations, and it must be able to use such facts
to draw conclusions about what plan will achieve a goal.

	Knowledge is only one of the areas in which the common  sense
facts  about  the world must be formalized.  It must also know how to
express the location and attitude of objects in space  and  the  laws
determining  the  effects of physical events on the objects.   Events
that occur in parallel and interact with one  another  offer  special
difficulties.

	2.   What  modes  of  reasoning  can the computer use to draw
conclusions from such facts - especially conclusions that a  plan  is
appropriate for achieving a goal?

	3.  How can a computer search a space of possible derivations
in order to draw a conclusion of a desired kind?  E.g. we want it  to
conclude  that  a  plan  is a good bet to achieve a goal, but it must
find the plan as well as draw the conclusion.  The main difficulty is
the  so-called  "combinatorial  explosion"  of possibilities, and the
main method is to use special knowledge  of  the  problem  domain  to
derive  "heuristics"  that  allow  a  program  to  tell whether it is
getting warmer or colder with a minimum of blind search.



The Stanford Artificial Intelligence Laboratory plans  the  following
basic research in formal reasoning:

FY 76 and 7T


	The Stanford work on general  facts  about  the  world,  will
concentrate  in  this  period  on  finding  the facts about knowledge
following up some earlier  successes  in  the  theory  of  knowledge.
Special attention will also be given to interacting events and to the
facts about the motion of material objects.

	The main  Stanford  tool  for  experimenting  with  modes  of
reasoning  is  a  program called FOL for checking chains of reasoning
expressed in the language of mathematical logic.  A  major  goal  for
this  period  is  to get the lengths of the derivations acceptable to
FOL down to the length of informal mathematical proofs  of  the  same
conclusions.    This has already required some new modes of reasoning
and using observations, and the required brevity is expected in  some
mathematical areas of reasoning in this period.

	The  general predicate calculus theorem prover which has been
used to prove mathematical results and is used in  Stanford  work  on
program  verification will have added a "hunch language" that permits
knowledge of the problem domain to guide the search for a derivation.


FY 77

	In this period, the Stanford group will try to make a general
inventory of the facts of the common  sense  world,  accepting  gross
simplifications  whenever  necessary  to  get  enough  facts to allow
reasoning about a general class of common sense problems.

	The proof-checker will have decision procedures added for the
most  important  decidable  domains of reasoning.  This will make the
computer checkable derivations shorter than informal ones as well  as
more  precise.    The inclusion of facts about parallel action should
permit the system to be applied to verifying programs  that  interact
with the real world.

	The  work  on the hunch language will continue. The new modes
of reasoning developed in connection with FOL will be  added  to  the
general prover.  This may require re-writing it.


FY 78-80

	In this period, it may be possible to combine the three lines
of  work  into a workable "advice taker" program that has long been a
goal of artificial intelligence research.  Such a program  will  have
enough   common   sense  knowledge  to  "understand"  most  practical
problems.  It will decide what to do by deriving a statement that  an
action  will  achieve  a goal, and this will include goals of getting
more information.  The program would be generally intelligent but not
very  intelligent,  because its heuristics probably won't be powerful
enough to solve difficult problems without excessive search, and  its
formalizations of common sense concepts will not be very precise.

	Even  at  this  time, work will still have to continue on the
formalization problem, on the modes of reasoning problem, and on  the
heuristic problem.


	This schedule  doesn't  allow  for  unforeseen  difficulties,
because  one  can't  tell  in what parts of the plan the difficulties
will arise.   The main application significance of this work  in  the
given  time  period  will  be  its influence on more applied AI work.
Namely, the concentration on finding out  the  facts  of  the  common
sense world and formalizing common sense reasoning will permit faster
progress in understanding  these  matters  than  projects  that  face
difficult  heuristic problems also.  Therefore, the work will provide
a scientific basis for more applied projects.